\begin{tabbing}
$\forall$\=$E$:Type, ${\it eq}$:EqDecider($E$), ${\it prd}$:($E$$\rightarrow$(?$E$)), ${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id))),\+
\\[0ex]${\it oax}$:EOrderAxioms($E$; ${\it prd}$; ${\it info}$), $T$:(Id$\rightarrow$Id$\rightarrow$Type), $w$, $a$:($x$:Id$\rightarrow$$e$:$E$$\rightarrow$$T$(loc($e$),$x$)),
\\[0ex]${\it sax}$:($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ ($\forall$$x$:Id. $w$($x$,$e$) = $a$($x$,pred($e$)) $\in$ $T$(loc($e$),$x$))),
\\[0ex]$V$:(Knd$\rightarrow$Id$\rightarrow$Type), $v$:($e$:$E$$\rightarrow$$V$(kind($e$),loc($e$))).
\-\\[0ex]mk{-}eval($E$;${\it eq}$;${\it prd}$;${\it info}$;${\it oax}$;$T$;$w$;$a$;${\it sax}$;$V$;$v$) $\in$ EventsWithValues
\end{tabbing}